Univalence Axiom (UA)
Univalence Axiom (UA)
同一性に関する公理の一つ
公理なので証明はされない？
Univalenceのいい訳し方は未だによくわからない
下記ページで自分の見解をメモしておく
→Univalence Axiomの訳
Univalence Axiomはホモトピー型理論で使われている
ホモトピー型理論は∞-トポスの内部言語
ホモトピー同値である型同士は同じ型であるとみなしてよいことを保証する公理([関山2024])
Univalent Foundationsの重要な公理の一つ？
定義はunivalence axiom in nLabを見る
$ (A =_\mathcal{U} B) \equiv (A \simeq B)
$ \mathrm{idtoequiv}(A,B): (A, B) \equiv (A \simeq B)
Univalence Axiom関連の動画
CIRM - Videos & books Library - Search by event(英語設定で検索)
CIRM - Videos & books Library - Dans tout Kentika(フランス語設定で検索)
Univalence Axiom(UA)に関するいろいろな実装
HoTTの実装
Coq-HoTT
Cubical Type Theoryの実装
Cubical Agda
Agda Unimath
UniMath/agda-unimath: The agda-unimath library
一価性公理 -- ホモトピー型理論
【1211.2851】 The Simplicial Model of Univalent Foundations (after Voevodsky)
Structuralism, Invariance, and Univalence
確認用
Q. Univalence Axiom
Q. 何がうれしいか
関連
Univalence
同値関係
宇宙型
型宇宙
依存型理論
可縮性
同一視型(identity type)
参考
univalence axiom in nLab
[関山2024] 『計算物理班 新たな数学としてのホモトピー型理論』Physics Lab. 2024
「同じ」を考える -- Univalence Axiom 入門 | MaruLabo
https://www.youtube.com/watch?v=LUcTKi-nGUQ
メモ
同一視型の基本定理 -- ホモトピー型理論
一価性 -- ホモトピー型理論
Univalence - 1Lab
#Homotopy_Type_Theory(HoTT)